$\forall$$A$:Realizer, $x$:Id.
\\[0ex]($\neg$($\uparrow$Rplus?($A$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($A$)))
\\[0ex]$\Rightarrow$ ($\uparrow$$x$ $\in$ dom(Rds($A$)))
\\[0ex]$\Rightarrow$ (inr $<$R{-}loc($A$), $x$$>$  $\in$ R{-}names($A$))